$\forall$$A$:Type, ${\it eq}$:EqDecider($A$), $B$:($A$$\rightarrow$Type), $x$, $y$:$A$, $v$:$B$($x$), $u$:$B$($y$).
\\[0ex]$x$ : $v$ $\parallel$ $y$ : $u$ $\Leftrightarrow$ ($x$ $=$ $y$ $\Rightarrow$ $v$ $=$ $u$ $\in$ $B$($x$))